Nuprl Lemma : local_or_rcv
11,40
postcript
pdf
k
:Knd. (
islocal(
k
))
(
isrcv(
k
))
latex
Definitions
x
:
A
.
B
(
x
)
,
Knd
,
b
,
islocal(
k
)
,
isrcv(
k
)
,
b
,
isl(
x
)
,
tt
,
ff
,
if
b
then
t
else
f
fi
,
t
T
,
P
Q
,
True
,
{
T
}
,
Lemmas
IdLnk
wf
,
Id
wf
,
false
wf
origin
k:Knd. (
islocal(k)) 
(isrcv(k)) k:Knd. (islocal(k)) (isrcv(k)) x:A. B(x)b
b
T Q